<!DOCTYPE html>
<!--
     SPDX-License-Identifier: CC-BY-SA-4.0
     SPDX-FileCopyrightText: 2020 seL4 Project a Series of LF Projects, LLC.
-->
<!-- Page last generated 2025-02-20 03:16:15 +0000 -->
<html lang="en">
  <head>
    <meta charset="utf-8">
    <meta http-equiv="X-UA-Compatible" content="IE=edge">
    <meta name="viewport" content="width=device-width, initial-scale=1">
    <title>Debugging guide | seL4 docs</title>

    <!-- Our stylesheet and theme stylesheet.  Contains bootstrap. -->
    <link rel="stylesheet" href="/assets/css/style.css" type="text/css">
    <!-- Font awesome -->
    <link href="https://use.fontawesome.com/releases/v5.0.8/css/all.css" rel="stylesheet">
    <link href="https://fonts.googleapis.com/css2?family=Roboto&display=swap" rel="stylesheet">
    <!-- Pygments syntax highlighting  -->
    <link rel="stylesheet" href="/assets/css/highlighting/trac.css" type="text/css">
    <link rel="icon" type="image/x-icon" href="/assets/favicon.ico"><script defer data-domain="docs.sel4.systems"
	    src="https://analytics.sel4.systems/js/script.js"></script></head>

  <body class="container-fluid">

    



<header>
  <ul class="row menu">
    <li class="col-xs-12 col-md-2" >
            <a href="https://sel4.systems" class="skip-icon">
              <img class="img-responsive" src="/assets/logo-text-white.svg" alt="seL4 logo" />
            </a>
    </li>
    <li class="col-xs-12 col-md-10 menu">
      <nav aria-label="Banner links">
        <h2><a href="/Resources" />Resources</h2>
        <h2><a href="/processes" />Contributing</a></h2>
        <h2><a href="/projects" />Projects</h2>
        <h2><a href="/Tutorials" />Tutorials</h2>
        <iframe title="DuckDuckGo search bar" src="https://duckduckgo.com/search.html?site=docs.sel4.systems&prefill=Search%20sel4.systems" style="overflow:hidden;margin-bottom:10px; padding:0;height:40px;float:right;border-width: 0px"></iframe>
      </nav>
    </li>
  </ul>
  <div class="clear"></div>
  
<div class="breadcrumbs bootstrap hidden-sm-down">
  <nav class="sel-breadcrumb" aria-label="Breadcrumb" >
    <ol class=" list-unstyled" vocab="http://schema.org/" typeof="BreadcrumbList">
      
      
        

        

        <li class="breadcrumb-item" property="itemListElement" typeof="ListItem">
            <a property="item" typeof="WebPage" href="/">
              <span property="name"><b>seL4 Docs</b></span>
            </a>
            <meta property="position" content="1" />
        </li>
      
        

        

        <li class="breadcrumb-item" property="itemListElement" typeof="ListItem">
            <a property="item" typeof="WebPage" href="/projects/">
              <span property="name"><b>Projects</b></span>
            </a>
            <meta property="position" content="2" />
        </li>
      
        

        
          <li class="breadcrumb-item" property="itemListElement" typeof="ListItem">
            <span property="name">Debugging guide</span>
            <meta property="position" content="3" /></li>
          
    </ol>
  </nav>
  <nav class="sel-version" aria-label="Current Versions">
    <ol class="list-unstyled">
      <li class="list-unstyled text-right" style="margin-left:auto; padding:0rem 0rem;">
        Current versions:</li>
      <li class="list-unstyled text-right">
      <a href="/releases/sel4/13.0.0"><b>seL4-13.0.0</b></a></li>
      <li class="list-unstyled text-right">
      <a href="/releases/microkit/1.4.1"><b>microkit-1.4.1</b></a></li>
      <li class="list-unstyled text-right">
      <a href="/releases/camkes/camkes-3.11.0"><b>camkes-3.11.0</b></a></li>
      <li class="list-unstyled text-right">
      <a href="/releases/capdl/0.3.0"><b>capDL-0.3.0</b></a></li>
      </ol>
  </nav>
  <div class='clear'></div>
</div>


</header>

    <main>
      <div class="row">
  <div class="hidden-xs col-sm-4 col-md-3 col-lg-2">
    

<div class="sidebar">
  <ul class="nav nav-sidebar tutorial-sidebar">
    <li class="nav-section">Getting started</li>
      <li><a href="/Tutorials/">Overview</a></li>
      <li><a href="/Tutorials/pathways">Tutorial pathways</a></li>
    <li class="nav-section">seL4</li>
      <li><a href="/Tutorials/setting-up">Setting up your machine</a></li>
      <li><a href="/Tutorials/get-the-tutorials">Getting the tutorials</a></li>
      <li><a href="/Tutorials/hello-world">Hello world</a></li>
      <li><a href="/Tutorials/capabilities">Capabilities</a></li>
      <li><a href="/Tutorials/untyped">Untyped</a></li>
      <li><a href="/Tutorials/mapping">Mapping</a></li>
      <li><a href="/Tutorials/threads">Threads</a></li>
      <li><a href="/Tutorials/ipc">IPC</a></li>
      <li><a href="/Tutorials/notifications">Notifications</a></li>
      <li><a href="/Tutorials/interrupts">Interrupts</a></li>
      <li><a href="/Tutorials/fault-handlers">Fault handling</a></li>
      <li><a href="/Tutorials/mcs">MCS extensions</a></li>
    <li class="nav-section">C Libraries</li>
      <li><a href="/Tutorials/libraries-1">Initialisation &amp; threading</a></li>
      <li><a href="/Tutorials/libraries-2">IPC</a></li>
      <li><a href="/Tutorials/libraries-3">Processes &amp; Elf loading</a></li>
      <li><a href="/Tutorials/libraries-4">Timer</a></li>
    <li class="nav-section">Microkit</li>
      <li><a href="https://trustworthy.systems/projects/microkit/tutorial/">Tutorial</a></li>
    <li class="nav-section">CAmkES</li>
      <li><a href="/Tutorials/hello-camkes-0">Hello CAmkES</a></li>
      <li><a href="/Tutorials/hello-camkes-1">Introduction to CAmkES</a></li>
      <li><a href="/Tutorials/hello-camkes-2">Events in CAmkES</a></li>
      <li><a href="/Tutorials/hello-camkes-timer">CAmkES timer tutorial</a></li>
      <li><a href="/Tutorials/camkes-vm-linux">CAmkES VM</a></li>
      <li><a href="/Tutorials/camkes-vm-crossvm">CAmkES cross-VM connectors</a></li>
    <li class="nav-section">Rust</li>
      <li><a href="https://github.com/seL4/rust-sel4">GitHub</a></li>
    <li class="nav-section">Resources</li>
      <li><a href="https://sel4.systems/Info/Docs/seL4-manual-latest.pdf">seL4 Manual</a></li>
      <li><a href="/projects/sel4/api-doc.html">seL4 API reference</a></li>
      <li><a href="/Tutorials/how-to">How to: a quick solutions guide</a></li>
      <li><a href="/projects/sel4-tutorials/debugging-guide">Debugging guide</a></li>
      <li><a href="/Resources#contact">Help contacts</a></li>
  </ul>
</div>

  </div>
  <div class="content col-sm-8 col-md-6 col-lg-7 main">

    <h1 id="debugging-guide">Debugging guide</h1>

<h2 id="compiler-settings">Compiler Settings</h2>

<p>Ensure that the build directory you are building in is not a release build. To
do so, check you build directory <code class="language-plaintext highlighter-rouge">CMakeCache.txt</code> file for the following lines:</p>

<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>* `CMAKE_BUILD_TYPE:STRING=Debug`
* `KernelDebugBuild:BOOL=ON`
</code></pre></div></div>

<p>Debug builds enable helpful features for debugging including:</p>

<ul>
  <li><code class="language-plaintext highlighter-rouge">printf</code> + a serial driver,</li>
  <li><code class="language-plaintext highlighter-rouge">-g</code> is passed to the compiler,</li>
  <li>compile- and run-time asserts,</li>
  <li>the kernel will print out error messages when invocations fail.</li>
</ul>

<h2 id="qemu">Qemu</h2>

<p><a href="http://www.qemu.org/">Qemu</a> is a simulator that provides
software emulation of a hardware platform. It is useful for developing
and debugging embedded software when you do not have access to the
target platform. Even if you do have the target hardware, Qemu can
shorten your edit-compile-debug cycle. Be aware that it is not
cycle-accurate and cannot emulate every device, so sometimes you have no
alternative than to debug on real hardware.</p>

<p>For the seL4 tutorials, a <code class="language-plaintext highlighter-rouge">simulate</code> script is always generated for use in the
build directory of a project. In most other projects, this script can be
generated by passing the flag <code class="language-plaintext highlighter-rouge">-DSIMULATION=1</code> to the <code class="language-plaintext highlighter-rouge">../init-build.sh</code> invocation.</p>

<div class="language-bash highlighter-rouge"><div class="highlight"><pre class="highlight"><code>    <span class="nb">mkdir </span>build_dir
    <span class="nb">cd </span>build_dir
    ../init-build.sh <span class="nt">-DSIMULATION</span><span class="o">=</span>1
    ./simulate
</code></pre></div></div>

<p>If the platform does not support qemu, the script will output</p>

<div class="language-bash highlighter-rouge"><div class="highlight"><pre class="highlight"><code>    Unsupported platform or architecture <span class="k">for </span>simulation
</code></pre></div></div>

<p>When simulating a seL4 system in Qemu, you should see output that is
directed to the (emulated) UART device on your terminal:</p>
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>ELF-loader started on CPU: ARM Ltd. ARMv6 Part: 0xb36 r1p3
  paddr=[82000000..8225001f]
ELF-loading image 'kernel'
  paddr=[80000000..80033fff]
  vaddr=[f0000000..f0033fff]
  virt_entry=f0000000
ELF-loading image 'sel4test-driver'
  paddr=[80034000..8036efff]
  vaddr=[10000..34afff]
  virt_entry=1c880
Enabling MMU and paging
Jumping to kernel-image entry point...

Bootstrapping kernel
Switching to a safer, bigger stack...
seL4 Test
=========
...
</code></pre></div></div>

<p>To exit from Qemu, type the sequence Ctrl+”a”, then “x”. Note that you
can exit at any point; you do not need to wait for the system to finish
or reach some stable state. If you exit Qemu while a system is running,
it will simply be terminated.</p>

<p>Qemu has some powerful debugging features built in. You can type
Ctrl+”a”, then “c” to switch to the Qemu monitor. From here you can
inspect CPU or device state, read and write memory, and single-step
execution. More information about this functionality is available in the
<a href="https://qemu-project.gitlab.io/qemu/system/monitor.html">Qemu documentation</a>.</p>

<p>When debugging a seL4 project, the Qemu debugger is inherently limited.
It has no understanding of your source code, so it is difficult to
relate what you are seeing back to the C code you compiled. It is
possible to get a richer debugging environment by connecting GDB to
Qemu.</p>

<h3 id="using-gdb-with-qemu">Using GDB with Qemu</h3>

<p><a href="https://www.gnu.org/s/gdb/">GDB</a> is a debugger commonly used
in C application development. Though not as seamless as debugging a
native Linux application, it is possible to use GDB to debug within
Qemu’s emulated environment.</p>

<p>Start Qemu with the extra options “-S” (pause execution on start) and
“-s” (start a GDB server on TCP port 1234):</p>
<div class="language-bash highlighter-rouge"><div class="highlight"><pre class="highlight"><code>./simulate <span class="nt">--extra-qemu-args</span><span class="o">=</span><span class="s2">"-S -s"</span>
</code></pre></div></div>

<p>In a separate terminal window, start your target platform’s version of
GDB. You should either pass a binary of the seL4 kernel if you intend on
debugging seL4 itself or the userspace application if you intend on
debugging an application on seL4.</p>

<p>In this example we’re going
to debug the seL4 kernel that has been built in debug mode:</p>
<div class="language-bash highlighter-rouge"><div class="highlight"><pre class="highlight"><code><span class="k">${</span><span class="nv">CROSS_COMPILER_PREFIX</span><span class="k">}</span>gdb kernel/kernel.elf
</code></pre></div></div>

<p>Where <code class="language-plaintext highlighter-rouge">CROSS_COMPILER_PREFIX</code> is the prefix used for the toolchain for the
architecture you are debugging. For x86 this is blank, for other architectures you can
check the <code class="language-plaintext highlighter-rouge">CMakeCache.txt</code> file in the build directory for the variable <code class="language-plaintext highlighter-rouge">CROSS_COMPILER_PREFIX</code>. In the following example, the prefix is <code class="language-plaintext highlighter-rouge">arm-none-eabi-</code>:</p>

<div class="language-bash highlighter-rouge"><div class="highlight"><pre class="highlight"><code>CROSS_COMPILER_PREFIX:UNINITIALIZED<span class="o">=</span>arm-none-eabi-
</code></pre></div></div>

<p>At the GDB prompt, enter “target remote :1234” to connect to the server
Qemu is hosting:</p>
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>Reading symbols from kernel/kernel.elf...done.
(gdb) target remote :1234
Remote debugging using :1234
0x82000000 in ?? ()
(gdb)
</code></pre></div></div>

<p>Suppose we want to halt when kprintf is called. Enter “break kprintf” at
the GDB prompt:</p>
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>(gdb) break kprintf
Breakpoint 1 at 0xf0011248: file kernel/src/machine/io.c, line 269.
</code></pre></div></div>

<p>We can now start Qemu running and wait until we hit the breakpoint. To
do this, type “cont” at the GDB prompt:</p>
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>(gdb) cont
Continuing.

Breakpoint 1, kprintf (format=0xf0428000 "") at kernel/src/machine/io.c:269
269     {
</code></pre></div></div>

<p>Note that some output has appeared in the other terminal window running
Qemu as it has partially executed. It may be surprising to see that some
printing somehow happened without our breakpoint triggering. The reason
for this is that output we’re seeing is from the ELF loader that runs
prior to the kernel. GDB does not know the address of its print function
(as we only gave GDB the kernel’s symbol table) and it is not looking to
break on its address. The breakpoint we have just hit is the first time
the ‘‘kernel’’ tried to print. Similarly, the breakpoint we have
configured will have no effect on userspace calls to <code class="language-plaintext highlighter-rouge">printf</code>.</p>

<p>Now that we are stopped at a breakpoint, all the standard GDB operations
are possible (inspect registers or the stack, single-step, continue
until function exit, …). More information is available in the
<a href="http://www.gnu.org/software/gdb/documentation/">GDB manual</a>.</p>

<p>Be warned that if you are debugging the kernel’s early boot steps,
something that may not be immediately obvious is that debugging across a
context in which page mappings change (e.g. switching page directories
or turning the MMU on/off) will confuse GDB and you may find breakpoints
triggering unexpectedly or being missed.</p>

<p>The process we have described is similar for x86, though if you are on
an x86 or x86_64 host you can simply use your platform’s native GDB,
gdb.</p>

<h4 id="userspace-debugging">Userspace debugging</h4>

<p>The steps for debugging a userspace application on seL4 are identical to
the ones we have just seen, except that we pass GDB a symbol table for
userspace rather than the kernel. For example, using the same sel4test
environment we start Qemu in the same way but start GDB with sel4test’s
binary:</p>
<div class="language-bash highlighter-rouge"><div class="highlight"><pre class="highlight"><code><span class="k">${</span><span class="nv">CROSS_COMPILER_PREFIX</span><span class="k">}</span>gdb projects/sel4test/apps/sel4test-driver/sel4test-driver
</code></pre></div></div>

<p>After connecting to Qemu, we can instruct GDB to break on the userspace
<code class="language-plaintext highlighter-rouge">printf</code> function:</p>
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>Reading symbols from projects/sel4test/apps/sel4test-driver/sel4test-driver.bin...done.
(gdb) target remote :1234
Remote debugging using :1234 0x82000000 in ?? ()
(gdb) break printf
Breakpoint 1 at 0x30870: file libs/libmuslc/src/stdio/printf.c, line 9.
(gdb)
</code></pre></div></div>

<p>Note that GDB has correctly identified the printf function in Musl C. We
now continue as before:</p>

<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>(gdb) cont
Continuing.

Breakpoint 1, printf (fmt=0x363e8 "%s") at libs/libmuslc/src/stdio/printf.c:9
9               ret = vfprintf(stdout, fmt, ap);
(gdb)
</code></pre></div></div>

<p>If you examine the terminal window running Qemu at this point, you will
note that we see an extra bit of output from the kernel. The kernel’s
print functionality is unaffected, but GDB has stopped execution the
first time userspace called <code class="language-plaintext highlighter-rouge">printf</code>.</p>

<p>From here, the experience is essentially identical to debugging the
kernel. One small complication to be aware of is that debugging across a
context switch may be confusing. If you are single-stepping in GDB and
find execution suddenly diverted to an address where code is unknown,
check the address itself. It is usually easy to identify from the
address alone when execution is in kernel code or the exception vector
table. Unfortunately there is no easy way to continue until you’re back
in userspace, particularly if the kernel schedules a different thread
than the one you were debugging. Depending on the scenario you are
debugging, it may be simpler to modify your system setup to ensure only
one thread is running.</p>

<h2 id="objdump">Objdump</h2>

<p>Objdump can be used to disassemble an ELF file, be it a kernel or an
application. This can be used to lookup the instruction where a fault
occurred. Make sure <code class="language-plaintext highlighter-rouge">-g</code> is passed to the compiler so that debug
information is included in the image.</p>

<p>Like gdb, the appropriate objdump from the toolchain must be called by
using <code class="language-plaintext highlighter-rouge">CROSS_COMPILER_PREFIX</code>.</p>

<p>For ARM, supposing that <strong>arm-none-eabi-</strong> is used as the
cross-compiler prefix.</p>
<div class="language-bash highlighter-rouge"><div class="highlight"><pre class="highlight"><code>arm-none-eabi-objdump <span class="nt">-D</span> binary_file_name <span class="o">&gt;</span> dump.s
</code></pre></div></div>
<p>For x86</p>
<div class="language-bash highlighter-rouge"><div class="highlight"><pre class="highlight"><code>objdump <span class="nt">-D</span> binary_file_name <span class="o">&gt;</span> dump.s
</code></pre></div></div>
<p>The file <code class="language-plaintext highlighter-rouge">dump.s</code> has the human-readable assembly instructions.</p>

<p>If you have symbols and want (C) source information in your disassembly
(and who doesn’t!) then use the -S flag. for example:</p>
<div class="language-bash highlighter-rouge"><div class="highlight"><pre class="highlight"><code><span class="k">${</span><span class="nv">CROSS_COMPILER_PREFIX</span><span class="k">}</span>objdump <span class="nt">-DS</span> binary_file_name
</code></pre></div></div>

<h2 id="hardware-debugging">Hardware debugging</h2>

<p>For some platforms, seL4 supports hardware debugging. See <a href="DebuggingUserspace">Hardware debugging of userspace threads</a>.</p>

<h2 id="in-kernel-debugging">In kernel debugging</h2>

<p>seL4 does not currently have a kernel debugger. As a result, most of our
debugging is done with:</p>

<ul>
  <li><code class="language-plaintext highlighter-rouge">objdump</code> as described above,</li>
  <li><code class="language-plaintext highlighter-rouge">printf</code>,</li>
  <li><code class="language-plaintext highlighter-rouge">__builtin_return_address</code> (to figure out stack traces).</li>
</ul>

<p>In the kernel, we provide <code class="language-plaintext highlighter-rouge">debug_printKernelEntryReason</code> found in
<a href="https://github.com/seL4/seL4/blob/master/include/api/debug.h">debug.h</a>
which can be used at any point in the kernel to output the current
operation that the kernel is doing.</p>


<p style="text-align: right;">

</p>


  </div>

  
    
<div class="sidebar-toc hidden-xs hidden-sm col-md-3 col-lg-3">
    <ul id="toc" class="section-nav">
<li class="toc-entry toc-h2"><a href="#compiler-settings">Compiler Settings</a></li>
<li class="toc-entry toc-h2"><a href="#qemu">Qemu</a>
<ul>
<li class="toc-entry toc-h3"><a href="#using-gdb-with-qemu">Using GDB with Qemu</a>
<ul>
<li class="toc-entry toc-h4"><a href="#userspace-debugging">Userspace debugging</a></li>
</ul>
</li>
</ul>
</li>
<li class="toc-entry toc-h2"><a href="#objdump">Objdump</a></li>
<li class="toc-entry toc-h2"><a href="#hardware-debugging">Hardware debugging</a></li>
<li class="toc-entry toc-h2"><a href="#in-kernel-debugging">In kernel debugging</a></li>
</ul>
</div>

  
</div>
<script src="/assets/js/toggle-markdown.js"></script>

    </main>
    


<footer class="site-footer">

  <h2 class="footer-heading">seL4 docs</h2>

  <div class="footer-col-wrapper">

    <div class="col-md-2">
      



<ul class="social-media-list">
  <li><a href="https://github.com/sel4"><i class="fab fa-github"></i> <span class="username">sel4</span></a></li><li><a href="https://github.com/sel4proj"><i class="fab fa-github"></i> <span class="username">sel4proj</span></a></li>
</ul>

    </div>

    <div class="col-md-8">
      <ul class="list-unstyled">
        <li>
          This site is for displaying seL4 related documentation.  Pull requests are welcome.
        </li>
        
          <li>
            Site last updated: Fri Feb 7 10:17:38 2025 +1100 ee78c8857c
          </li>
          <li>
                Page last updated: Mon Jan 6 18:52:01 2025 +1100 df31e5ccb8
          </li>
        
      </ul>
    </div>
    <div class="col-md-2">
<a href="https://github.com/seL4/docs/blob/master/projects/sel4-tutorials/debugging-guide.md">View page on GitHub</a>
      <br />
      <a href="https://github.com/seL4/docs/edit/master/projects/sel4-tutorials/debugging-guide.md">Edit page on GitHub</a>
      <br />
      <a href="/sitemap">Sitemap</a>
    </div>

  </div>

</footer>

  </body>
</html>
